\begin{tabbing}
interleaved\_family\_occurence($T$;$I$;$L$;$L_{2}$;$f$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=($\forall$$i$:$I$. increasing($f$($i$);$\parallel$$L$($i$)$\parallel$) \& ($\forall$$j$:\{0..$\parallel$$L$($i$)$\parallel^{-}$\}. ($L$($i$))[$j$] $=$ $L_{2}$[$f$($i$,$j$)] $\in$ $T$))\+
\\[0ex]\& (\=$\forall$$i_{1}$:$I$, $i_{2}$:$I$.\+
\\[0ex]$\neg$$i_{1}$ $=$ $i_{2}$ $\in$ $I$
\\[0ex]$\Rightarrow$ ($\forall$$j_{1}$:\{0..$\parallel$$L$($i_{1}$)$\parallel^{-}$\}, $j_{2}$:\{0..$\parallel$$L$($i_{2}$)$\parallel^{-}$\}. $\neg$$f$($i_{1}$,$j_{1}$) $=$ $f$($i_{2}$,$j_{2}$) $\in$ $\mathbb{Z}$))
\-\\[0ex]\& ($\forall$$x$:\{0..$\parallel$$L_{2}$$\parallel^{-}$\}. $\exists$$i$:$I$, $j$:\{0..$\parallel$$L$($i$)$\parallel^{-}$\}. $x$ $=$ $f$($i$,$j$) $\in$ $\mathbb{Z}$)
\-
\end{tabbing}